$\forall$${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$, ${\it e'}$:E. Dec($R$(${\it e'}$,$e$)))
\\[0ex]$\Rightarrow$ $R$ =$>$ $\lambda$$x$,$y$. ($x$ $<$ $y$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. Dec(es{-}r{-}immediate{-}pred(${\it es}$;$R$;${\it e'}$;$e$)))